# encoding=gbk
#`基于http://aima.cs.berkeley.edu示例代码`

import collections
from collections import defaultdict, Counter
from tkinter import *

# #创建主窗口
# top = Tk()
# top.title("命题逻辑推理系统") #标题设置
# top.geometry('300x100') #设置窗口大小为300x100 横纵尺寸
# #调用主事件循环，让窗口程序保持运行。
# top.mainloop()

class Expr:
    def __init__(self, op, *args): #`表达式包含操作符和若干参数`
        self.op = str(op)
        self.args = args

    def __invert__(self):                 #`重载逻辑非`
        return Expr('~', self)

    def __and__(self, rhs):               #`重载逻辑与`
        return Expr('&', self, rhs)

    def __or__(self, rhs):                #`重载逻辑或`
        if isinstance(rhs, Expr):
            return Expr('|', self, rhs)
        else:   #`处理$==>$类符号，$A==>$B已经转为$A|'==\>'|B$ `
            return PartialExpr(rhs, self)

    def __eq__(self, other):
        return isinstance(other,Expr)and self.op==other.op\
               and self.args == other.args

    def __hash__(self):
        return hash(self.op) ^ hash(self.args)

    def __repr__(self):
        op = self.op
        args = [str(arg) for arg in self.args]
        if op.isidentifier():  # f(x) or f(x, y)
            return '{}({})'.format(op, ', '.join(args)) \
                   if args else op
        elif len(args) == 1:  # -x or -(x + 1)
            return op + args[0]
        else:  # (x - y)
            opp = (' ' + op + ' ')
            return '(' + opp.join(args) + ')'

class PartialExpr:

    def __init__(self, op, lhs):
        self.op, self.lhs = op, lhs

    def __or__(self, rhs):
        return Expr(self.op, self.lhs, rhs)

    def __repr__(self):
        return "PartialExpr('{}', {})".format(\
            self.op, self.lhs)


def expr(x):
    if isinstance(x, str):
        for op in ['==>', '<==', '<=>']:
            x = x.replace(op, '|' + repr(op) + '|')
        return eval(x, defaultkeydict(Symbol))
        #`eval用符号分割子串，子串作为原子命题。`
    else:
        return  x

def Symbol(name):  #`处理原子命题`
     return Expr(name)

class defaultkeydict(collections.defaultdict):
    #`类似defaultdict,但是使用default\_factory 来对key进行处理。`
    def __missing__(self, key):
        self[key] = result = self.default_factory(key)
        return result

    def __missing__(self, key):
        self[key] = result = self.default_factory(key)
        return result

class KB:
    def __init__(self, sentence=None,explain4):
        self.rules = []                           #`储存规则`
        if sentence:
            self.tell(sentence)

    def tell(self, sentence):                     #`增加规则`
        self.rules.append(expr(sentence))

    def ask(self, query):                         #`通过枚举方法检查是否可以推导出query`
        return tt_entails(Expr('&', *self.rules), expr(query))

    def explain(self,explainText):
        return

def tt_entails(kb, alpha):                        #`由KB推导出alpha`
    symbols = list(prop_symbols(kb & alpha))      #`分解所有的命题词`
    return tt_check_all(kb, alpha, symbols, {})   #`枚举所有命题词的各种赋值，并检查kb是蕴含alpha`

def prop_symbols(x):
    if not isinstance(x, Expr):
        return set()
    elif is_prop_symbol(x.op):   #`原子语句，操作符为单命题词`
        return {x}
    else:                        #`符合语句，递归分解操作参数`
        return {symbol for arg in x.args
                for symbol in prop_symbols(arg)}

def tt_check_all(kb, alpha, symbols, model):
    if not symbols:              #`各命题词都已纳入了模型`
        if pl_true(kb, model):   #`模型满足kb`
            result = pl_true(alpha, model) #`是否满足语句alpha`
            assert result in (True, False)
            return result
        else:
            return True
    else:                     #`递归，枚举每个命题词的不同赋值`
        P, rest = symbols[0], symbols[1:]
        model[P]=True
        res1=tt_check_all(kb, alpha, rest, model)
        model[P]=False
        res2=tt_check_all(kb, alpha, rest, model)
        return res1 and res2

def is_prop_symbol(s):           #`命题词是首字母大写`
    return isinstance(s, str) and s[0].isupper()

def pl_true(exp, model={}):
    #`exp是一个表达式，model是一个以命题词为key的词典`
    if exp in (True, False):
        return exp
    op, args = exp.op, exp.args
    if is_prop_symbol(op):       #`原子语句`
        return model.get(exp)
    elif op == '~':
        p = pl_true(args[0], model)
        if p is None:
            return None
        else:
            return not p
    elif op == '|':
        result = False
        for arg in args:
            p = pl_true(arg, model)
            if p is True:
                return True
            if p is None:
                result = None
        return result
    elif op == '&':
        result = True
        for arg in args:
            p = pl_true(arg, model)
            if p is False:
                return False
            if p is None:
                result = None
        return result

    p, q = args                             #`到此时应是蕴含表达式`
    if op == '==>':
        return pl_true(~p | q, model)       #`根据公式\ref{e_imp}处理$=>$`

    pt = pl_true(p, model)                  #`根据公式\ref{e_eqv}处理$<=>$`
    if pt is None:
        return None
    qt = pl_true(q, model)
    if qt is None:
        return None
    if op == '<=>':
        return pt == qt
    else:
        raise ValueError(
            'Illegal operator in logic expression' + str(exp))

if __name__ == '__main__':
    s=expr('A11&B')
    print(s)
    kb=KB()

    kb.tell('Q|P')
    kb.tell('T')
    kb.tell('P==>(~R)')
    kb.tell('S==>(~T)')
    kb.tell('~S==>R')

    print(kb.rules)
    print(kb.ask('P'))
    print(kb.ask('Q'))
    # kb.tell('~P11')
    # kb.tell('~B11')
    # kb.tell('B21')
    # kb.tell('B11<=>(P12|P21)')
    # kb.tell('B21<=>(P11|P22|P31)')
    #
    # print(kb.rules)
    # # print(kb.ask('~P12'))
    # print(kb.ask('P21'))
    # print(kb.ask('P22'))
    # print(kb.ask('~P21'))
    # print(kb.ask('~P22'))
    # # print(kb.ask('~B21'))
    # # print(kb.ask('B21'))
    # # print(kb.ask('P44'))

